\begin{tabbing}
$\forall$\=${\it es}$:ES, $e_{1}$, $e_{2}$, $b$:E, $Q$,\+
\\[0ex]$P$:(\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}$\rightarrow$\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}$\rightarrow$Prop).
\-\\[0ex]($e_{1}$ $<$loc $b$)
\\[0ex]$\Rightarrow$ $b$ $\leq$ $e_{2}$ 
\\[0ex]$\Rightarrow$ [$e_{1}$;pred($b$)]$\sim$([$a$,$b$].$P$($a$,$b$))$\ast$[$a$,$b$].$P$($a$,$b$)
\\[0ex]$\Rightarrow$ [$b$;$e_{2}$]$\sim$([$a$,$b$].$P$($a$,$b$))$\ast$[$a$,$b$].$Q$($a$,$b$)
\\[0ex]$\Rightarrow$ [$e_{1}$;$e_{2}$]$\sim$([$a$,$b$].$P$($a$,$b$))$\ast$[$a$,$b$].$Q$($a$,$b$)
\end{tabbing}